(set-logic QF_BV)
(declare-fun _substvar_30507_ () Bool)
(declare-fun _substvar_30509_ () Bool)
(declare-fun _substvar_33587_ () Bool)
(declare-fun _substvar_36494_ () Bool)
(declare-fun _substvar_36503_ () Bool)
(declare-fun _substvar_36516_ () Bool)
(declare-fun _substvar_36520_ () Bool)
(declare-fun _substvar_37159_ () Bool)
(declare-fun _substvar_37280_ () Bool)
(declare-fun _substvar_38372_ () Bool)
(declare-fun _substvar_38373_ () Bool)
(declare-fun _substvar_38399_ () Bool)
(declare-fun _substvar_38427_ () Bool)
(declare-fun _substvar_38440_ () Bool)
(declare-fun _substvar_39006_ () Bool)
(declare-fun _substvar_39174_ () Bool)
(declare-fun |Scoreboard#7#9886| () Bool)
(declare-fun |Scoreboard#13#9888| () (_ BitVec 1))
(declare-fun |Scoreboard#14#9889| () (_ BitVec 1))
(declare-fun |$paramod/FF/WIDTH=1#0#9891| () Bool)
(declare-fun |$paramod/FF/WIDTH=1#1#9893| () (_ BitVec 1))
(declare-fun |$paramod/FF/WIDTH=1#3#9899| () Bool)
(declare-fun |$paramod/MagicPacketTracker/DEPTH=8#1#9904| () Bool)
(declare-fun |Scoreboard#21#9927| () Bool)
(define-fun |$paramod/MagicPacketTracker/DEPTH=8_h#9982| () Bool (and _substvar_38372_ _substvar_38373_ _substvar_39174_ (= |$paramod/MagicPacketTracker/DEPTH=8#1#9904| _substvar_37280_) _substvar_39006_))
(assert (and _substvar_38399_ (= (= (bvor (ite |Scoreboard#7#9886| #b1 #b0) (bvand |Scoreboard#13#9888| |Scoreboard#14#9889|)) #b1) |$paramod/FF/WIDTH=1#0#9891|) (= |Scoreboard#7#9886| (= |$paramod/FF/WIDTH=1#1#9893| #b1)) _substvar_38427_ _substvar_37159_ _substvar_38440_ _substvar_36494_ _substvar_36503_ _substvar_36516_ _substvar_36520_ (= |Scoreboard#21#9927| _substvar_30507_) _substvar_30509_ |$paramod/MagicPacketTracker/DEPTH=8_h#9982| _substvar_33587_))
(declare-fun |$paramod/FF/WIDTH=1#1#10246| () (_ BitVec 1))
(assert (= |$paramod/FF/WIDTH=1#1#10246| #b1))
(assert (= (ite |$paramod/FF/WIDTH=1#3#9899| (ite |$paramod/FF/WIDTH=1#0#9891| #b1 #b0) |$paramod/FF/WIDTH=1#1#9893|) |$paramod/FF/WIDTH=1#1#10246|))
(check-sat)
(exit)
